(set-logic QF_BV)
(declare-fun _substvar_78_ () (_ BitVec 8))
(declare-fun _substvar_68_ () (_ BitVec 8))
(declare-fun _substvar_82_ () (_ BitVec 32))
(declare-fun _substvar_80_ () (_ BitVec 32))
(declare-fun _substvar_76_ () (_ BitVec 32))
(declare-fun _substvar_64_ () (_ BitVec 32))
(assert (= _substvar_80_ ((_ sign_extend 24) _substvar_78_)))
(assert (= _substvar_76_ _substvar_80_))
(assert (= _substvar_64_ _substvar_76_))
(assert (= _substvar_68_ ((_ extract 7 0) _substvar_64_)))
(assert (= _substvar_82_ ((_ sign_extend 24) _substvar_68_)))
(assert (= (_ bv0 32) (bvadd _substvar_82_ ((_ extract 31 0) (_ bv24 64)))))
(check-sat)
(exit)
